T:Type, L:(T List), n:int_iseg(0; ||L||). append(firstn(n; L); nth_tl(n;L)) = L 

latex

Definitions	Y, True, P  Q, False, P  Q, A, A  B, prop{i:l}, t  T, append(as; bs), int_iseg(i; j), x:A. B(x)
Lemmas	length wf1, bnot wf, le wf, assert wf, bool wf, le int wf